﻿using System;
using System.Diagnostics;
using System.Collections.Generic;

using alib.Debugging;
using alib.Enumerable;

namespace agree
{
	using F = Edge.Flag;

	///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
	/// <summary>
	/// TFS subsumption checking for (e.g.) packing purposes
	/// </summary>
	/// <reference>
	/// Stephan Oepen, John Carroll. 2000. "Ambiguity Packing in Constraint-based Parsing--Practical Results."
	/// In Proceedings of the 1st North American chapter of the Association for Computational Linguistics 
	/// conference. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 162-169. 
	/// </reference>
	///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
	public unsafe sealed class Subsumption
	{
		[ThreadStatic]
		static Subsumption _inst;

		public const int None = 0;
		public const int FirstSubsumesSecond = 1;
		public const int SecondSubsumesFirst = 2;
		public const int Equivalent = 3;
		public const int Bottom = -4;	// note: doesn't interfere with subsumption bit-testing

		const int FirstNotSubsuming = ~FirstSubsumesSecond;
		const int SecondNotSubsuming = ~SecondSubsumesFirst;

		Subsumption() { }

		TypeUtils tu;
		int subsumption, next_id;
		int* rgb0, rgb1;
		ushort** rgpfix;
		arr_tfs_entry* pate0, pate1;
		ushort* phf0, phf1;
		int c0, c1;
#if DEBUG
		int c_alloc;
#endif

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// 
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		void _init(Restrictor r, int c0, int c1)
		{
			this.rgpfix = r.R;
			this.tu = r.FeatMgr.tu;
			this.subsumption = Equivalent;
			this.rgb0 = this.rgb1 = null;
			this.next_id = 0;
			this.c0 = c0;
			this.c1 = c1;
#if DEBUG
			this.c_alloc = c0 + c1;
#endif
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// 
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		bool _halt(F f, int m0, int m1)
		{
			if ((f & F.EtmNonBareType) == 0 || m0 == 0 || m1 == 0)
				return false;
			int nm0, nm1;
			ushort* pfix = *(ushort**)((long)rgpfix + ((int)f << 3));
			do
			{
				f = _check_types(
							ArrayTfs.TryGetFlagsMark(phf0, pate0, *pfix, m0, out nm0), nm0,
							ArrayTfs.TryGetFlagsMark(phf1, pate1, *pfix, m1, out nm1), nm1);
			}
			while (subsumption > 0 && !_halt(f, nm0, nm1) && *++pfix != 0xFFFF);
			return subsumption <= 0;
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// 
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		F _check_types(F f0, int nm0, F f1, int nm1)
		{
			int* pb0, pb1;
			if (f0 < 0 && f1 < 0)
			{
#if DEBUG
				if (~nm0 >= c_alloc || c0 + ~nm1 >= c_alloc)
					throw new Exception();
#endif
				int b0 = *(pb0 = (int*)((byte*)rgb0 + (~nm0 << 2)));
				int b1 = *(pb1 = (int*)((byte*)rgb1 + (~nm1 << 2)));
				if (b0 + b1 == 0)
				{
					next_id++;
					*pb0 = next_id;
					*pb1 = next_id;
				}
				else if (b0 == 0)
				{
					subsumption &= SecondNotSubsuming;
					if (subsumption <= 0)
						return 0;
					*pb0 = b1;
				}
				else if (b1 == 0)
				{
					subsumption &= FirstNotSubsuming;
					if (subsumption <= 0)
						return 0;
					*pb1 = b0;
				}
				else if (b0 != b1)
				{
					subsumption = None;
					return 0;
				}
				f0 &= F.IdResolve;
				f1 &= F.IdResolve;
			}
			else if (f0 < 0)
			{
#if DEBUG
				if (~nm0 >= c_alloc)
					throw new Exception();
#endif
				subsumption &= FirstNotSubsuming;
				if (subsumption <= 0)
					return 0;
				if (*(pb0 = (int*)((byte*)rgb0 + (~nm0 << 2))) == 0)
				{
					next_id++;
					*pb0 = next_id;
				}
				f0 &= F.IdResolve;
			}
			else if (f1 < 0)
			{
#if DEBUG
				if (c0 + ~nm1 >= c_alloc)
					throw new Exception();
#endif
				subsumption &= SecondNotSubsuming;
				if (subsumption <= 0)
					return 0;
				if (*(pb1 = (int*)((byte*)rgb1 + (~nm1 << 2))) == 0)
				{
					next_id++;
					*pb1 = next_id;
				}
				f1 &= F.IdResolve;
			}

			/// now that the coreference bit is stripped out, check type subsumption
			if (f0 == f1)
				return f0;
			if (f1 == 0)
			{
				subsumption &= FirstNotSubsuming;
				return f0;
			}
			if (f0 == 0)
			{
				subsumption &= SecondNotSubsuming;
				return f1;
			}

			F f;
			if ((f0 & f1) >= F.EtmLeafType ||
				(f = f1 < f0 ? tu.UnifyTypesHiLo(f1, f0) : tu.UnifyTypesHiLo(f0, f1)) < 0)
			{
				subsumption = Bottom;
				return F.Bottom;
			}
			else if (f == f0)
				subsumption &= FirstNotSubsuming;
			else if (f == f1)
				subsumption &= SecondNotSubsuming;
			else
				subsumption = None;
			return f;
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		///
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		void _check(Edge e0, Edge e1)
		{
			F f = _check_types(e0.FlagsId, e0.Mark, e1.FlagsId, e1.Mark);
			if (subsumption <= 0)
				return;

			int* _pp = stackalloc int[c0 + c1];
			rgb0 = _pp;
			rgb1 = _pp + c0;
			_halt(f, e0.Mark, e1.Mark);
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// 
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		void _check_subsumption_pairs(IEnumerable<Pairing<ITfsSlot>> rgpr)
		{
			int* _pp = stackalloc int[c0 + c1];
			rgb0 = _pp;
			rgb1 = _pp + c0;
			foreach (var pr in rgpr)
			{
				Edge e0 = pr.x.Edge();
				Edge e1 = pr.y.Edge();
				F f = _check_types(e0.FlagsId, e0.Mark, e1.FlagsId, e1.Mark);
				if (subsumption <= 0 || _halt(f, e0.Mark, e1.Mark))
					break;
			}
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// <summary>
		/// -4 : tfs0 ⊓ tfs1 = ⊥
		///  0 : no subsumption relationship (possibly ⊥)
		///  1 : tfs0 ⊑ tfs1
		///  2 : tfs1 ⊑ tfs0
		///  3 : tfs0 == tfs1
		/// </summary>
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		public static int Check(Restrictor r, ITfsSlot ts0, ITfsSlot ts1)
		{
			Subsumption s;
			if ((s = _inst) == null)
				_inst = s = new Subsumption();

			var a0 = (ArrayTfs)ts0.Tfs;
			var a1 = (ArrayTfs)ts1.Tfs;

			s._init(r ?? a0.ftm.r_none, a0.c_corefs, a1.c_corefs);

			fixed (ushort* _phf0 = a0.h.pfirst, _phf1 = a1.h.pfirst)
			fixed (arr_tfs_entry* _pate0 = a0.entries, _pate1 = a1.entries)
			{
				s.pate0 = _pate0; s.phf0 = _phf0;
				s.pate1 = _pate1; s.phf1 = _phf1;
				s._check(ts0.SlotIndex == 0 ? a0._top_edge : _pate0[ts0.SlotIndex - 1].e,
						 ts1.SlotIndex == 0 ? a1._top_edge : _pate1[ts1.SlotIndex - 1].e);
			}
			return s.subsumption;
		}

		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		/// <summary>
		/// 
		/// </summary>
		///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
		public static int CheckSubsumptionPairs(Restrictor r, IEnumerable<Pairing<ITfsSlot>> rgpr)
		{
			Subsumption s;
			if ((s = _inst) == null)
				_inst = s = new Subsumption();

			var e = rgpr.GetEnumerator();
			if (!e.MoveNext())
				throw new Exception();

			var tfs0 = (ArrayTfs)e.Current.x.Tfs;
			var tfs1 = (ArrayTfs)e.Current.y.Tfs;

			s._init(r, tfs0.c_corefs, tfs1.c_corefs);

			fixed (ushort* _phf0 = tfs0.h.pfirst, _phf1 = tfs1.h.pfirst)
			fixed (arr_tfs_entry* _pate0 = tfs0.entries, _pate1 = tfs1.entries)
			{
				s.pate0 = _pate0;
				s.pate1 = _pate1;
				s.phf0 = _phf0;
				s.phf1 = _phf1;
				s._check_subsumption_pairs(rgpr);
			}
			return s.subsumption;
		}
	};
}
